"""
modify : 2020_11_14
Author : _int_me
注：量词后必须用括号将辖域指出,并且不能存在变元名称冲突
"""

import re
import sys


class MyError(Exception):  # 自定义异常
    def __init__(self, value):
        self.value = value

    def __str__(self):
        return repr(self.value)


Sig = r"=>|&"
M_words = r"∀∃"
Sig2 = r"!()"
X_re = re.compile(r"[A-Z][(][a-z][)]")  # 谓词检验正则
UP_re = re.compile(r"[A-Z]")  # 大写字母检验正则
LO_re = re.compile(r"[a-z]")  # 小写字母检验正则
A_ton = dict()  # 谓词映射
cnt = 0  # 变元个数
xs = set()  # 变元集合


class Tree:
    def __init__(self, p_str):
        global Sig
        global M_words
        global X_re
        self.P_str = p_str
        self.F = True
        self.m_words = []
        self.leaf = False
        if p_str == "":
            return
        seg = []
        while True:
            last = 0
            sta = 0
            for j in range(len(p_str)):  # 括号匹配与有效区间提取
                if p_str[j] == '(':
                    if sta == 0:
                        seg.append([last, j])
                    sta += 1
                if p_str[j] == ')':
                    if sta == 0:
                        raise MyError("Error parentheses match in " + p_str)
                    else:
                        sta -= 1
                        if sta == 0:
                            last = j + 1
            if sta != 0:
                raise MyError("Error parentheses match in " + p_str)
            if last == len(p_str):
                if not seg:
                    p_str = p_str[1: -1]
                    continue
                elif len(seg) > 1:
                    break
                else:
                    temp_str = p_str[seg[0][0]: seg[0][1]]
                    if not re.search(UP_re, temp_str):
                        self.F = (temp_str.count('!') % 2 == 1) ^ self.F
                        M_a = temp_str.find('∀')
                        M_b = temp_str.find('∃')
                        st = 0
                        if M_a == -1 and M_b == -1:
                            pass
                        else:
                            if M_a == -1:
                                st = M_b
                            elif M_b == -1:
                                st = M_a
                            else:
                                st = min(M_a, M_b)
                        M_F = st % 2 == 0
                        p_str = p_str[st:]
                        cnt = len(temp_str) - st
                        while cnt > 0:
                            if p_str[0] in M_words:
                                if not M_F:
                                    p_str = M_words[1 - M_words.find(p_str[0])] + p_str[1:]
                                if p_str[2:].find(p_str[1]) != -1:  # 保留有效量词
                                    self.m_words.append(p_str[: 2])
                                p_str = p_str[2:]
                            if p_str[0] == '!':
                                p_str = p_str[1:]
                            cnt -= 1
                        cnt = 0
                        while p_str[cnt] != '(':
                            cnt += 1
                        p_str = p_str[cnt + 1: -1]
                        seg = []
                        continue
                    else:
                        break
            else:
                seg.append([last, len(p_str)])
                break
        while p_str[0] == '!':  # 存储否定
            self.F = not self.F
            p_str = p_str[1:]
        self.P_str = '(' + p_str + ')'
        sp = -1
        for i in Sig:
            for j in seg:
                sp = p_str[j[0]: j[1]].find(i)
                if sp != -1:
                    sp += j[0]
                    break
            if sp != -1:
                self.opt = i
                l_str = p_str[: sp]
                r_str = p_str[sp + 1:]
                if self.opt == '>':  # 去掉蕴含
                    if not self.F:
                        r_str = "!(" + r_str + ')'
                        self.opt = '&'
                        self.F = True
                    else:
                        l_str = "!(" + l_str + ')'
                        self.opt = '|'
                if (not self.F) and self.opt in {'&', '|'}:  # 德摩根律
                    self.opt = list({'&', '|'} - {self.opt})[0]
                    self.F = True
                    l_str = "!(" + l_str + ')'
                    r_str = "!(" + r_str + ')'

                try:
                    self.L = Tree(l_str)
                    self.R = Tree(r_str)
                    self.m_words.extend(self.L.m_words)  # 简单的量词扩张（直接上提）
                    self.m_words.extend(self.R.m_words)
                    self.L.m_words = []
                    self.R.m_words = []
                    break
                except MyError as err:
                    raise err
        if sp == -1:
            self.leaf = True
            return

    def calc(self, flag):  # 计算真值
        global A_ton
        if self.leaf:
            return ((flag & (1 << A_ton[self.P_str])) != 0) ^ (not self.F)
        else:
            res_l = self.L.calc(flag)
            res_r = self.R.calc(flag)
            if self.opt == '&':
                return (res_l and res_r) ^ (not self.F)
            elif self.opt == '|':
                return (res_l or res_r) ^ (not self.F)
            else:
                return (res_l == res_r) ^ (not self.F)

    def display(self):  # 输出表达式
        for i in self.m_words:
            print(i, end="")
        if not self.F:
            print("!", end="")
        if self.leaf:
            print(self.P_str, end="")
            return
        else:
            print('(', end="")
            self.L.display()
            print(self.opt, end="")
            self.R.display()
            print(')', end="")


Ps = []
Pre_trs = []
Pre_exp = ""
Des = ""
Pre_tr = Tree("")
Des_tr = Tree("")
Pre_M_exp = ""
Des_M_exp = ""


def pre_to_pro():
    global Ps
    global Des_tr
    global Pre_trs
    global Des
    global xs

    a_list = list(set(map(chr, range(ord('a'), ord('n') + 1))) - xs)  # 用差集得到可用常元列表
    x_list = list(set(map(chr, range(ord('o'), ord('z') + 1))) - xs)  # 用差集得到可用变元列表

    new_Ps = []
    del_Ps = []
    index = 0
    for i in Pre_trs:
        if i.m_words:
            print("检测到前提中的前束范式：  ", end="")
            i.display()
            print("\n请输入期望的替换公式(必要条件,第一行输入需要添加的公式数量n，第二行为n个空格隔开的序号)\n(若除此之外需要其他公式，请在n之后输入 other)")
            formulas = []
            for j in i.m_words:
                if j[0] == '∃':
                    i.P_str.replace(j[1], a_list[0])
                    xs.add(a_list[0])
                    del a_list[0]
            ssv = ""
            for j in i.m_words:
                if j[0] == '∀':
                    if ssv == "":
                        ssv = j[1]
                        break
            if ssv != "":
                for j in list(xs):
                    if j != ssv:
                        adds = ""
                        if not i.F:
                            adds = "!"
                        formulas.append(adds + i.P_str.replace(ssv, j))
                        print("{}: {}".format(len(formulas), formulas[-1]))
            else:
                adds = ""
                if not i.F:
                    adds = "!"
                formulas.append(adds + i.P_str)
                print("{}: {}".format(1, formulas[-1]))

            ss = input().split(" ")
            if ss[0] != '0':
                ssn = input().split(" ")
                for j in range(int(ss[0])):
                    new_Ps.append(formulas[int(ssn[j]) - 1])
            if len(ss) > 1:
                ss_other = int(input("请输入其他公式的数量(之后每行输入一个公式，无量词)："))
                for j in range(ss_other):
                    new_Ps.append(input())
                    xs |= set(LO_re.findall(new_Ps[-1]))
                    a_list = list(set(a_list) - set(LO_re.findall(new_Ps[-1])))
                    x_list = list(set(x_list) - set(LO_re.findall(new_Ps[-1])))

            del_Ps.append(Ps[index])
            index += 1
    Ps = list(set(Ps) - set(del_Ps))
    Ps.extend(new_Ps)

    if Des_tr.m_words:
        print("检测到结论中的前束范式：  ", end="")
        Des_tr.display()
        print("\n请输入期望的替换公式(充分条件)(序号n)\n(若除此之外需要其他公式，请输入 other)")

        formulas = []
        ssv = ""
        for j in Des_tr.m_words:
            if j[0] == '∃':
                if ssv == "":
                    ssv = j[1]
                    break
        if ssv != "":
            for j in list(xs):
                if j != ssv:
                    adds = ""
                    if not Des_tr.F:
                        adds = "!"
                    formulas.append(adds + Des_tr.P_str.replace(ssv, j))
                    print("{}: {}".format(len(formulas), formulas[-1]))
        else:
            adds = ""
            if not Des_tr.F:
                adds = "!"
            formulas.append(adds + Des_tr.P_str)
            print("{}: {}".format(1, formulas[-1]))

        ss = input()
        if ss == "other":
            Des = input("请输入其他公式(无量词)：")
            xs |= set(LO_re.findall(Des[-1]))
        else:
            Des = formulas[int(ss) - 1]


def m_exp():
    global Des_tr
    global Pre_tr
    global Des
    global Pre_exp
    global A_ton
    global Pre_M_exp
    global Des_M_exp
    global cnt
    Pre_real = set()
    Des_real = set()
    fl = True

    results1 = X_re.findall(Pre_exp)
    results1.extend(X_re.findall(Des))
    results1 = list(set(results1))

    for i in results1:
        A_ton['(' + i + ')'] = cnt
        cnt += 1

    mx = (1 << cnt)
    for i in range(mx):
        if not Pre_tr.calc(i):
            Pre_real.add(i)
            Pre_M_exp += "("
            for j in range(cnt):
                if (1 << j) & i != 0:
                    Pre_M_exp += "!(" + results1[j] + ')' + '|'
                else:
                    Pre_M_exp += "(" + results1[j] + ')' + '|'
            Pre_M_exp = Pre_M_exp[: -1] + ")&"
    Pre_M_exp = Pre_M_exp[: -1]

    for i in range(mx):
        if not Des_tr.calc(i):
            if i not in Pre_real:
                fl = False
            Des_real.add(i)
            Des_M_exp += "("
            for j in range(cnt):
                if (1 << j) & i != 0:
                    Des_M_exp += "!(" + results1[j] + ')' + '|'
                else:
                    Des_M_exp += "(" + results1[j] + ')' + '|'
            Des_M_exp = Des_M_exp[: -1] + ")&"
    Des_M_exp = Des_M_exp[: -1]

    return fl


def pre_handle():
    global Ps
    global Des
    global Des_tr
    global Pre_trs
    global xs

    for i in Ps:
        xs |= set(LO_re.findall(i))  # 统计变元
        try:
            Pre_trs.append(Tree(i))
        except MyError as err:
            print(err.value)
            return False

    xs |= set(LO_re.findall(Des))
    try:
        Des_tr = Tree(Des)
    except MyError as err:
        print(err.value)
        return False

    return True


def after_handle():
    global Ps
    global Des
    global Pre_exp
    global Des_tr
    global Pre_trs
    global Pre_tr

    for i in Ps:
        try:
            Pre_trs.append(Tree(i))
        except MyError as err:
            print(err.value)
            return False
        Pre_exp += '(' + i + ')&'
    Pre_exp = Pre_exp[:-1]
    try:
        Pre_tr = Tree(Pre_exp)
    except MyError as err:
        print(err.value)
        return False
    try:
        Des_tr = Tree(Des)
    except MyError as err:
        print(err.value)
        return False

    return True


if __name__ == "__main__":
    print("*" * 16, "有限NL系统_v2.0", "*" * 16)
    print("请输入前提(最后一行为单独的P字母)")
    ss = input()
    while ss != "P":
        Ps.append(ss)
        ss = input()
    print("请输入结论(一行)")
    Des = input()

    if not pre_handle():
        print("Exit with a pre_handle error")
        sys.exit(0)

    print()
    pre_to_pro()
    print('\n')

    if not after_handle():
        print("Exit with a after_handle error")
        sys.exit(0)

    if m_exp():
        print("推理结果：正确")
        print("证明如下：\n")

        i = 0
        while i < len(Ps):
            print("[{}] {}\n(前提引入)".format(i + 1, Ps[i]), end="\n\n")
            i += 1
        print(("[{}] {}\n(置换规则 " + ("[{}] " * len(Ps))[: -1]).format(i + 1, Pre_exp, *(range(1, len(Ps) + 1))),
              end=")\n\n")
        i += 1
        print("[{}] {}\n(置换规则 [{}])".format(i + 1, Pre_M_exp, i), end="\n\n")

        if len(Pre_M_exp) > len(Des_M_exp):  # 如果不完全等价 则需要化简律
            i += 1
            print("[{}] {}\n(化简律   [{}])".format(i + 1, Des_M_exp, i), end="\n\n")
        i += 1
        print("[{}] {}\n(置换规则 [{}])".format(i + 1, Des, i), end="\n\n")
    else:
        print("推理结果：错误")

    print("\nBye")
